(***************************************************************************
 * Cast-Free Featherweight Java
 *
 * Bruno De Fraine, with help from Erik Ernst and Mario Sudholt, Summer 2008
 ***************************************************************************)

Require Import AdditionalTactics.
Require Import Metatheory.
Require Import FJ_Definitions.

(** * auxiliary facts *)

Scheme typing_typings_ind := Minimality for typing Sort Prop
with wide_typing_typings_ind := Minimality for wide_typing Sort Prop
with wide_typings_typings_ind := Minimality for wide_typings Sort Prop.

Combined Scheme typings_mutind from typing_typings_ind, 
wide_typing_typings_ind, wide_typings_typings_ind.

Fact typings_implies_ok_env:
    (forall E tE e t A, typing E tE e t A -> ok tE) /\
    (forall E tE e t A, wide_typing E tE e t A -> ok tE) /\
    (forall E tE es ts A, wide_typings E tE es ts A -> ok tE).
Proof.
  apply typings_mutind; intros; trivial.
Qed.

Definition typing_implies_ok_env := 
  proj1 typings_implies_ok_env.
Definition wide_typing_implies_ok_env := 
  proj1 (proj2 typings_implies_ok_env).
Definition wide_typings_implies_ok_env := 
  proj2 (proj2 typings_implies_ok_env).

Hint Immediate typing_implies_ok_env 
     wide_typing_implies_ok_env 
     wide_typings_implies_ok_env.

Hint Resolve binds_other.

Fact ok_class_meth: 
  forall C D fs ms m t E tE e k ns,
    ok_tclass C D fs k ms ns ->
    binds m (E,t,tE,e) ms ->
    ok_meth E t m tE e (t_C C).
Proof.
  intros.
  unfold ok_tclass in H.
  fold (ok_meth' (t_C C) m (E,t,tE,e)).
  eapply fa_binds_elim. 
  eassumption.
  destruct H as [A [gs [_ [_ [H' _]]]]].
  assumption.
Qed.

Hint Resolve ok_class_meth.

Fact ok_nclass_meth: 
  forall C D fs ms m t E tE e k ns F fs' k' ms',
    ok_tclass C D fs k ms ns ->
    ok_nclass F fs' k' ms' C ->
    binds m (E,t,tE,e) ms' ->
    ok_meth E t m tE e (t_CdotC C F).
Proof.
  intros.
  unfold ok_tclass in H.
  fold (ok_meth' (t_CdotC C F) m (E,t,tE,e)).
  eapply fa_binds_elim. 
  eassumption.
  destruct H as [A [gs [_ [_ [H' _]]]]].
  unfold ok_nclass in H0.
  destruct H0 as [gs' [D' [_ [_ [_ [_ H2]]]]]].
  assumption.
Qed.

Hint Resolve ok_nclass_meth.

Fact ok_ctable_class: 
  forall ct C D fs ms k ns,
    ok_cenv ct ->
    binds C (D,fs,k,ms,ns) ct ->
    ok_tclass C D fs k ms ns.
Proof.
  intros.
  destruct H as (_, H).
  fold (ok_tclass' C (D,fs,k,ms,ns)).
  eapply fa_binds_elim;
    eassumption.
Qed. 

Fact ok_ctable_nclass: 
  forall ct C D fs ms k ns F fs' k' ms',
    ok_cenv ct ->
    binds C (D,fs,k,ms,ns) ct ->
    binds F (fs',k',ms') ns ->
    ok_nclass F fs' k' ms' C.
Proof.
  intros.
  inversion H.
  fold (ok_nclass' C F (fs',k',ms')).
  eapply fa_binds_elim.
    eassumption.
  assert (H4 := ok_ctable_class _ _ _ _ _ _ _ H H0).
  unfold ok_tclass in H4.
  destruct H4 as [A [gs [_ [_ [_ [H4 _]]]]]].
  assumption.
Qed. 

Hint Resolve ok_ctable_nclass.

(** ** Correspondence between keys and images of the same environment *)
Fact wide_typings_implies_zip: 
  forall E0 tE0 E es A,
    wide_typings E0 tE0 es (imgs E) A ->
    typeis_qcname A -> 
    exists Eds, env_zip E es Eds.
Proof.
  intros. 
  generalize dependent es.
  induction E; intros; inversion H; subst; eauto.
  destruct (IHE es0); eauto.
  destruct a. 
  eauto.
Qed.

Lemma tiq_sub_trans:
  forall E A B, 
    typeis_qcname A -> 
    sub E A B -> 
    typeis_qcname B.
Proof.
  intros E A B H H0.
  induction H0.
  assumption.
  inversion H.
  eauto.
  apply IHsub2.
  apply IHsub1.
  assumption.
  apply tiq_C.
Qed.

Hint Resolve tiq_sub_trans.

Hint Resolve wide_typings_implies_zip.

Fact binds_zip: 
  forall E0 E tE0 ds Eds v t A,
    typeis_qcname A ->
    wide_typings E0 tE0 ds (imgs E) A ->
    env_zip E ds Eds ->
    binds v t E ->
    (exists2 e, binds v e Eds & wide_typing E0 tE0 e t A).
Proof.
  intros E0 E tE0 ds Eds v t. 
  revert ds Eds.
  induction E; 
    intros; 
    [ | destruct a as (a0,t0)]; inversion H2.
    inversion H1. 
    subst. 
    inversion H0. 
    subst.
    destruct (v == a0).
      subst injections. 
      eauto using binds_first.
    destruct IHE with (1:=H) (2:=H13) (3:=H9).
    eauto.
    eauto.
Qed.

Hint Resolve binds_zip.

Fact binds_no_binds_false:
  forall m (env:benv) (t:type) (tenv:tenv) (exp:exp)  ms,
    binds m (env,t,tenv,exp) ms -> 
    no_binds m ms -> False.
Proof.
  intros.
  unfold binds, no_binds in *.
  rewrite H0 in H.
  discriminate.
Qed.

Hint Resolve binds_no_binds_false.

(** ** Properties that follow from the [ct_noobj] hypothesis *)
Module Type NoObj.
    Parameter ct_noobj: no_binds Object CT.
End NoObj.

Module NoObjFacts (Import H: NoObj).

    Fact binds_object:
      forall X,
        binds Object X CT -> False.
    Proof.
      intros X H.
      assert (no_binds Object CT).      
      apply ct_noobj.
      unfold no_binds in H0.
      unfold binds in H.
      rewrite H in H0.
      discriminate.
    Qed.

    Hint Resolve binds_object.

    Fact obj_nofields : 
      forall flds, 
        fields (t_C Object) flds -> flds = nil.
    Proof.
      intros.
      inversion H; subst.
      reflexivity.
      apply binds_object in H1.
      contradiction.
    Qed.

    Hint Resolve obj_nofields.

    Fact objdotC_nofields :
      forall C fs,
        fields (t_CdotC Object C) fs -> nil = fs.
    Proof.
      intros C fs H.
      inversion H; subst.
      reflexivity.
      apply binds_object in H2.
      contradiction.
      apply binds_object in H2.
      contradiction.      
    Qed.

    Hint Resolve objdotC_nofields.

    Fact field_object:
      forall f t,
        field (t_C Object) f t -> False.
    Proof.
      intros.
      inversion H.
      apply obj_nofields in H0.
      subst.
      inversion H1.
    Qed.

    Hint Resolve field_object.

    Fact obj_nomeths : 
      forall m env tenv t e, 
        ~ method m (t_C Object) env t tenv e.
    Proof.
      unfold not.
      intros.
      inversion H;
        subst;
        eauto.
    Qed.

    Hint Resolve obj_nomeths.

    Fact ok_class_empty: 
      forall C, 
        ok_tclass C Object nil (C,nil) nil nil.
    Proof.
      unfold ok_tclass.
      intro.
      exists (t_C C), nil.
      split.
      rewrite app_nil_r.
      reflexivity.
      split.
      apply f_tobject.
      split.
      apply fa_nil.
      split.
      apply fa_nil. 
      split.
      simpl.
      apply I.
      apply wf_object.
    Qed.

    Hint Resolve ok_class_empty.
    
    Fact fields_fun: 
      forall t fs fs',
        fields t fs -> 
        fields t fs' -> 
        fs = fs'.
    Proof.
      intros t fs fs' H H'.
      revert fs' H'.
      induction H; 
        intros; 
        inversion H'; 
        subst;
        try (reflexivity || exfalso; 
             eapply binds_object; eassumption).

      assert ((D,fs,c,ms,ns) = (D0,fs0,c0,ms0,ns0)) 
        by (eapply binds_fun; eassumption).
      subst injections.

      rewrite (IHfields gs0).
      reflexivity.
      assumption.

      assert ((D,hs,c,ms,ns) = (D0,hs0,c0,ms0,ns0)) 
        by (eapply binds_fun; eassumption).
      subst injections.

      rewrite (IHfields gs0).

      assert ((fs0,c'0,ms'0) = (fs,c',ms')) 
        by (eapply binds_fun; eassumption).
      subst injections.
      
      reflexivity.
      assumption.

      assert ((D,hs,c,ms,ns) = (D0,fs0,c0,ms0,ns0)) 
        by (eapply binds_fun; eassumption).
      subst injections.

      unfold no_binds in H5.
      unfold binds in H0.
      rewrite H0 in H5.
      discriminate.

      assert ((D,fs,c,ms,ns) = (D0,hs,c0,ms0,ns0)) 
        by (eapply binds_fun; eassumption).
      subst injections.

      unfold binds in H5.
      unfold no_binds in H0.
      rewrite H0 in H5.
      discriminate.

      assert ((D,fs,c,ms,ns) = (D0,fs0,c0,ms0,ns0)) 
        by (eapply binds_fun; eassumption).
      subst injections.      

      rewrite (IHfields fs').
      reflexivity.
      assumption.
    Qed.

    Hint Resolve fields_fun.
    
End NoObjFacts.

(** * Other properties and generalized typing rules *)

(** The generalized typing rules recreate the ordinary term typing rules, but require a [wide_typing] in place of a [typing] in the conditions. They usually follow from the property that subtyping preserves methods, fields,... *)
Fact method_fun: 
  forall m T env env' t t' tenv tenv' e e',
    method m T env t tenv e -> 
    method m T env' t' tenv' e'-> 
    env = env' /\ t = t' /\ tenv = tenv' /\ e = e'.
Proof.
  intros m T env env' t t' tenv tenv' e e' H H'.
  induction H;
    inversion H'; subst;
    try assert ((D,fs,c,ms,ns) = (D0,fs0,c0,ms0,ns0))
      by (eapply binds_fun; eassumption); subst injections.
  
  assert ((env,t,tenv,e) = (env',t',tenv',e'))
    by (eapply binds_fun; eassumption); subst injections.
  split. reflexivity. split. reflexivity. split; reflexivity.    
  
  contradiction by (eauto using binds_nobinds).
  contradiction by (eauto using binds_nobinds).
  eapply IHmethod.
  eassumption.

  assert ((fs',c',ms') = (fs'0,c'0,ms'0))
    by (eapply binds_fun; eassumption); subst injections.

  assert ((env,t,tenv,e) = (env',t',tenv',e'))
    by (eapply binds_fun; eassumption); subst injections.

  split. reflexivity. split. reflexivity. split; reflexivity.

  assert ((fs',c',ms') = (fs'0,c'0,ms'0))
    by (eapply binds_fun; eassumption); subst injections.

  contradiction by (eauto using binds_nobinds).
  contradiction by (eauto using binds_nobinds).

  eapply IHmethod.
  assert ((fs',c',ms') = (fs'0,c'0,ms'0))
    by (eapply binds_fun; eassumption); subst injections.
  contradiction by (eauto using binds_nobinds).

  eapply IHmethod.
  assert ((fs',c',ms') = (fs'0,c'0,ms'0))
    by (eapply binds_fun; eassumption); subst injections.
  assumption.

  contradiction by (eauto using binds_nobinds).
  contradiction by (eauto using binds_nobinds).
  contradiction by (eauto using binds_nobinds).
  
  eapply IHmethod.
  assumption.
Qed.

Hint Resolve method_fun.

Module OkTableAndNoObjFacts (Import H: Hyps).
    Module Import Facts1 := NoObjFacts H.

    Fact extends_fields: 
      forall C D fsv,
        extends C D ->
        fields (t_C D) fsv -> 
        exists fs, 
          fields (t_C C) (fsv ++ fs).
    Proof.
      intros.
      unfold extends in H.
      destruct H as [a [b [c [d e]]]].
      apply (f_tclass _ _ _ fsv) in e.      
      exists a.
      assumption.
      assumption.
    Qed.

    Inductive super_list : list scname -> Prop :=
    | sl_object : super_list (Object :: nil)
    | sl_extends : forall C D supers,
        extends C D ->
        super_list (D :: supers) ->
        super_list (C :: D :: supers).

    Hint Constructors super_list.

    Lemma super_list_from_fields:
      forall T fs,
        fields T fs ->
        forall C, T = (t_C C) ->
                  exists sl, super_list (C :: sl).
    Proof.
      intros T fs H.
      induction H;
        intros;
        subst injections.

      exists nil.
      eauto.

      destruct (IHfields D (eq_refl (t_C D))) as [sl' Hsl].
      exists (D :: sl').
      apply sl_extends.
      unfold extends.
      exists fs, c, ms, ns.
      eauto.
      assumption.
      
      inversion H.
      inversion H2.
      inversion H2.
    Qed.

    Lemma binds_forall_class:
      forall P,
        forall_env P CT ->
        forall C CD,
          binds C CD CT ->
          P C CD.
    Proof.
      intros P H.
      induction H;
        intros.
      inversion H.
      case (C == x).
      intro.
      subst.
      assert (binds x v ((x, v) :: E)).
      apply binds_first.
      apply binds_fun with (a:=v)in H1.
      subst.
      assumption.
      assumption.

      intro.
      eapply binds_elim_neq in H1.
      apply IHforall_env.
      assumption.
      assumption.
    Qed.

    Lemma binds_forall_nclass:
      forall P ns,
        forall_env P ns ->
        forall C (CD:(fenv*kenv*menv)),
          binds C CD ns ->
          P C CD.
    Proof.
      intros P ns H.
      induction H;
        intros.
      inversion H.
      case (C == x).
      intro.
      subst.
      assert (binds x v ((x, v) :: E)).
      apply binds_first.
      apply binds_fun with (a:=v)in H1.
      subst.
      assumption.
      assumption.

      intro.
      eapply binds_elim_neq in H1.
      apply IHforall_env.
      assumption.
      assumption.
    Qed.

    Lemma binds_forall_method:
      forall P ms,
        forall_env P ms ->
        forall C (CD:(benv*type*tenv*exp)),
          binds C CD ms ->
          P C CD.
    Proof.
      intros P ms H.
      induction H;
        intros.
      inversion H.
      case (C == x).
      intro.
      subst.
      assert (binds x v ((x, v) :: E)).
      apply binds_first.
      apply binds_fun with (a:=v)in H1.
      subst.
      assumption.
      assumption.

      intro.
      eapply binds_elim_neq in H1.
      apply IHforall_env.
      assumption.
      assumption.
    Qed.


    Lemma ok_implies_super_list:
      forall E C A, 
        ok_type E (t_C C) A ->
        exists sl, super_list (C :: sl).
    Proof.
      intros.
      remember (t_C C) as T.      
      induction H;
        subst injections.

      exists nil.
      eauto.

      destruct cd as [[[[D fs] c] ms] ns].
      assert (ok_cenv CT).
      apply ok_ct.
      assert (ok_tclass' C (D,fs,c,ms,ns)).
      unfold ok_cenv in H0.
      destruct H0.
      apply binds_forall_class.
      assumption.
      assumption.
      assert (ok_tclass C D fs c ms ns).
      unfold ok_tclass' in H1.
      assumption.
      unfold ok_tclass in H2.
      destruct H2 as [A' [gs [H3 [H4 H5]]]].

      assert (exists sl', super_list (D :: sl')).
      apply (super_list_from_fields (t_C D) gs H4 D (eq_refl (t_C D))).
      destruct H2 as [sl' H5'].
      exists (D :: sl').
      apply sl_extends.
      unfold extends.
      exists fs, c, ms, ns.
      assumption.
      assumption.
      
      inversion HeqT.
      inversion HeqT.
      inversion HeqT.
      inversion HeqT.
      inversion HeqT.
    Qed.      

    Lemma fields_from_super_list:
      forall C sl sl', 
        sl = C :: sl' ->
        super_list sl ->
        exists fs : fenv, fields (t_C C) fs.
    Proof.
      intros.
      revert C sl' H H0.
      induction sl; intros.
        inversion H.
                       
      destruct sl as [ | D sl].
        inversion H0; subst.
        subst injections.
        exists nil.
        eauto.

      subst injections.
      inversion H0; subst.
      assert (H3:=H2).
      unfold extends in H2.
      destruct H2 as [fs [c [ms [ns Hb]]]].      

      assert (exists fs0, fields (t_C D) fs0).
      apply (IHsl D sl).
      reflexivity.
      assumption.

      inversion H.
      exists (x ++ fs).
      apply (f_tclass C D fs x c ms ns).
      assumption.
      assumption.
    Qed.

    Lemma fields_tdef:
      forall E C A, 
        ok_type E (t_C C) A ->
        exists fs, fields (t_C C) fs.
    Proof.
      intros.
      inversion H; subst.
        exists nil.
        eauto.
      assert (Hsl := ok_implies_super_list _ _ _ H).
      destruct Hsl as [sl Hsl].
      remember (C::sl) as sl1.
      apply (fields_from_super_list C sl1 sl).
      assumption.
      assumption.
    Qed.
    
    Lemma ok_type_nested_top:
      forall E C D A,
        ok_type E (t_CdotC C D) A ->
        ok_type E (t_C C) A.
    Proof.
      intros.
      inversion H;
        subst.
      apply (wf_ccls E _ _ A) in H3.
      assumption.
      apply (wf_ccls E _ _ A) in H3.
      assumption.
    Qed.

    Inductive super_nesting_list : scname -> list scname ->
                                   list scname -> Prop :=
    | snl_nil : forall D,
        super_nesting_list D (Object :: nil) nil 
    | snl_cons_omit : forall C C' D sl sl' fs c ms ns, 
        super_list (C :: sl) ->
        binds C (C',fs,c,ms,ns) CT ->
        no_binds D ns ->
        super_nesting_list D sl sl' ->
        super_nesting_list D (C :: sl) sl' 
    | snl_cons_include : forall C C' D sl sl' cd fs c ms ns,
        super_list (C :: sl) ->
        binds C (C',fs,c,ms,ns) CT ->
        binds D cd ns ->
        super_nesting_list D sl sl' ->
        super_nesting_list D (C :: sl) (C :: sl').

    Lemma exists_super_nesting_list:
      forall sl0,
        super_list sl0 ->
        forall sl C D,
          sl0 = C :: sl ->
          exists sl', super_nesting_list D (C :: sl) sl'.
    Proof.
      intros sl0 H.
      induction H;
        intros.
      inversion H; subst.
      exists nil.
      apply snl_nil.

      inversion H1; subst.
      clear H1.
      unfold extends in H.
      destruct H as [fs [c [ms [ns H ]]]].

      remember (get D0 ns) as opt.
      destruct opt.
      destruct p as [[fsp cp] msc].

      assert (exists sl', super_nesting_list D0 (D :: supers) sl').
      apply (IHsuper_list supers D D0).
      reflexivity.
      destruct H1 as [sl' H1].
      exists (C0 :: sl').
      eapply snl_cons_include.
      apply (sl_extends C0) in H0.
      eassumption.
      unfold extends.
      exists fs, c, ms, ns.
      assumption.
      eassumption.
      unfold binds.
      symmetry.
      eassumption.
      assumption.

      assert (exists sl', super_nesting_list D0 (D :: supers) sl').
      apply (IHsuper_list supers D D0).
      reflexivity.
      destruct H1 as [sl' H1].
      exists sl'.
      eapply snl_cons_omit.
      apply (sl_extends C0) in H0.
      eassumption.
      unfold extends.
      exists fs, c, ms, ns.
      assumption.
      eassumption.
      unfold no_binds.
      symmetry.
      assumption.
      assumption.
    Qed.

    Lemma fields_ndef_from_super_nesting_list:
      forall sl0 sl' D,
        super_nesting_list D sl0 sl' ->
        forall C sl,
          sl0 = C :: sl ->
          exists fs : fenv, fields (t_CdotC C D) fs.
    Proof.
      intros sl0 sl' D H.
      induction H;
        intros.

      inversion H; subst.
      exists nil.
      eauto.

      inversion H3; subst.
      rename C0 into C, IHsuper_nesting_list into IHs.
      clear H3.
      destruct sl0.
      inversion H2.
      assert (s = C').
      inversion H; subst.
      unfold extends in H5.
      destruct H5 as [fs0 [c0 [ms0 [ns0 Hbinds]]]].
      assert ((s,fs0,c0,ms0,ns0) = (C',fs,c,ms,ns))
        by (eapply binds_fun; eassumption); subst injections.
      reflexivity.
      subst s.
      
      assert (exists fs1, fields (t_CdotC C' D) fs1).
      apply (IHs C' sl0).
      reflexivity.
      destruct H3 as [fs1 H3].
      exists fs1.
      eapply f_nsuper.
      eassumption.
      assumption.
      assumption.

      inversion H3; subst.
      clear H3.
      rename C0 into C.
      destruct cd as [[fsD cD] msD].
      cut(exists fs0 fs1, fields (t_CdotC C D) (fs0 ++ fs1)).
      intros.
      destruct H3 as [fs0 [fs1 H3]].
      exists (fs0 ++ fs1).
      assumption.

      rename IHsuper_nesting_list into IHs.
      destruct sl0.
      inversion H2.
      assert (s = C').
      inversion H; subst.
      unfold extends in H5.
      destruct H5 as [fs0 [c0 [ms0 [ns0 Hbinds]]]].
      assert ((s,fs0,c0,ms0,ns0) = (C',fs,c,ms,ns))
        by (eapply binds_fun; eassumption); subst injections.
      reflexivity.
      subst s.
      
      assert (exists fs0, fields (t_CdotC C' D) fs0).
      apply (IHs C' sl0).
      reflexivity.
      destruct H3 as [fs0 H3].
      exists fs0, fsD.
      eauto.
    Qed.

    Lemma fields_ndef_from_super_list:
      forall sl E C D A,
      ok_type E (t_CdotC C D) A ->
      super_list (C :: sl) ->
      exists fs : fenv, fields (t_CdotC C D) fs.
    Proof.
      intros.
      assert (Hx : exists sl', super_nesting_list D (C :: sl) sl').
      apply (exists_super_nesting_list (C::sl) H0 sl C D).
      reflexivity.
      destruct Hx as [sl' Hx].
      eapply (fields_ndef_from_super_nesting_list 
                (C::sl) sl' D Hx C sl).
      reflexivity.
    Qed.

    Lemma fields_ndef:
      forall E C D A, 
        ok_type E (t_CdotC C D) A ->
        exists fs, fields (t_CdotC C D) fs.
    Proof.
      intros.
      assert (H' := H).
      apply ok_type_nested_top in H'.
      assert (Hsl := ok_implies_super_list _ _ _ H').
      inversion Hsl.
      apply (fields_ndef_from_super_list x E C D A).
      assumption.
      assumption.
    Qed.
        
    Fact fields_def:
      forall E T A, 
        ok_type E T A ->
        typeis_qcname T ->
        exists fs, fields T fs.
    Proof.
      intros.
      inversion H0; subst.
      eauto using fields_tdef.
      eauto using fields_ndef.
    Qed.

    Lemma ok_type_weaken:
      forall F E G t A,
        ok (F ++ E ++ G) ->
        ok_type (F ++ G) t A ->
        ok_type (F ++ E ++ G) t A.
    Proof.
      intros.
      induction H0.
      eauto.
      eauto.
      eauto.
      eauto.
      apply wf_var with (C:=C).
      apply (binds_weaken G E F) in H0.
      assumption.
      assumption.
      assumption.
      apply (wf_absfam (F++E++G) X C D).
      assumption.
      apply (binds_weaken G E F) in H1.
      assumption.
      assumption.
      assumption.
      eauto.
    Qed.
    
    Lemma binds_ct_implies_binds:
      forall C D fs c ms ns,
        binds C (D, fs, c, ms, ns) CT ->
        D = Object \/
        exists E fs' c' ms' ns', binds D (E, fs', c', ms', ns') CT.
    Proof.
      intros.
      assert (Hok : ok_cenv CT).
      apply ok_ct.
      assert (ok_tclass' C (D,fs,c,ms,ns)).
      unfold ok_cenv in Hok.
      destruct Hok.
      apply binds_forall_class.
      assumption.
      assumption.
      assert (ok_tclass C D fs c ms ns).
      unfold ok_tclass' in H0.
      assumption.
      unfold ok_tclass in H1.
      destruct H1 as [A' [_ [_ [_ [_ [_ [_ H1]]]]]]].
      inversion H1; subst.
        eauto.
      destruct cd.
      destruct p.
      destruct p.
      destruct p.
      right.
      exists s, f, k, m, n.
      assumption.
    Qed.

    Lemma sub_object_object:
      forall E S T,
        sub E S T ->
        S = t_C Object ->
        T = t_C Object.
    Proof.
      intros E S T H.
      induction H;
        intros.
              assumption.
            inversion H0.
          reflexivity.
        apply IHsub2;
            apply IHsub1;
            assumption.
      subst injections.
      exfalso.
      apply binds_object with (X:=(D, fs, c, ms, ns)).
      assumption.
    Qed.

    Lemma sub_ok_implies_ok:
      forall E S T A,
        sub E S T ->
        ok_type E S A ->
        exists A', ok_type E T A'.
    Proof.
      intros.
      revert A H0.
      induction H; intros; subst; eauto.
      inversion H0; subst; eauto.
      eapply binds_fun in H; eauto. subst.
      eauto.
      assert (IH := IHsub1 A H1).
      destruct IH as [A' IH].
      apply (IHsub2 A').
      assumption.
      assert (Hok : ok_cenv CT).
      apply ok_ct.
      assert (ok_tclass' C (D,fs,c,ms,ns)).
      unfold ok_cenv in Hok.
      destruct Hok.
      apply binds_forall_class.
      assumption.
      assumption.
      assert (ok_tclass C D fs c ms ns).
      unfold ok_tclass' in H1.
      assumption.
      unfold ok_tclass in H2.
      destruct H2 as [A' [_ [_ [_ [_ [_ [_ H2]]]]]]].
      exists A'.
      assert (Hb := binds_ct_implies_binds _ _ _ _ _ _ H).
      destruct Hb.
        subst.
        eauto.
      destruct H3 as [F [fs' [c' [ms' [ns' H3]]]]].
      eauto.
      Grab Existential Variables.
      apply T.
    Qed.

    Lemma sub_ok_implies_ok':
      forall E S T A,
        sub E S T ->
        T <> t_C Object ->
        ok_type E T A ->
        exists A', ok_type E S A'.
    Proof.
      intros E S T A H.
      revert A.
      induction H; intros; subst; eauto.
      unfold not in H.
      exfalso. apply H. reflexivity.
      destruct (IHsub2 _ H1 H2) as [A' IH].
      apply (IHsub1 A').
      unfold not.
      intro.
      subst.
      assert (He := sub_object_object _ _ _ H0 eq_refl).
      subst.
      unfold not in H1.
      apply H1. reflexivity.
      assumption.
      Grab Existential Variables.
      apply A.
    Qed.

    (** ** Subtyping preserves fields *)
    Fact sub_fields: 
      forall E u v fsv A,
        typeis_qcname u ->
        sub E u v -> 
        fields v fsv -> 
        ok_type E u A ->
        exists fs, 
          fields u (fsv ++ fs).
    Proof.
      intros E u v fsv A Hqcn H Hf Hok.
      revert fsv A Hqcn Hf Hok.
      induction H; intros.

      exists nil.
      rewrite <- app_nil_end. 
      assumption.

      inversion Hqcn.

      apply obj_nofields in Hf.
      subst.
      simpl.
      eauto using fields_def.

      destruct (sub_ok_implies_ok _ _ _ _ H Hok).
      destruct (IHsub2 fsv x).
      eauto.
      assumption.
      assumption.
      
      destruct (IHsub1 (fsv ++ x0) A).
      assumption.
      assumption.
      assumption.
      exists (x0 ++ x1).
      rewrite app_assoc_reverse in H3.
      assumption.

      eauto.
    Qed.

    Hint Resolve sub_fields.

    Fact sub_field: 
      forall E u v f t A,
        typeis_qcname u ->
        sub E u v ->
        ok_type E u A ->
        field v f t -> 
        field u f t.
    Proof.
      unfold field. 
      intros.
      destruct H2.
      destruct (sub_fields E u v x A H H0 H2 H1).
      eauto using binds_head.
    Qed.

    Hint Resolve sub_field.

    Lemma eval_bound_tiq:
      forall a b c, 
        eval_bound a b c -> 
        typeis_qcname c.
    Proof.
      intros.
      inversion H; subst.
      assumption.
      eauto.
      eauto.
    Qed.

    Hint Resolve eval_bound_tiq.      

    Lemma eval_at_inversion:
      forall s t u,
        eval_at (s,t) u ->
        match u with
          | t_C C => s = t_C C
          | t_X X => s = t_X X
          | t_CdotC C D => s = t_CdotC C D \/
                           exists D', s = t_dotC D /\
                                      t = t_CdotC C D'
          | t_XdotC X D => s = t_XdotC X D \/
                           exists D', s = t_dotC D /\
                                      t = t_XdotC X D'
          | t_dotC C => s = t_dotC C /\ 
                        exists D', t = t_dotC D'
        end.
    Proof.
      intros.
      destruct u;
        inversion H;
        subst;
        eauto.
    Qed.

    Lemma type_dec:
      forall (s t:type),
        s = t \/ s <> t.
    Proof.
      intros.
      destruct s as [s|s|s|s|s];
        destruct t as [t|t|t|t|t];
        case (s == t);
        try case (s0 == s1);
        intros;
        subst;
        try (left; reflexivity);
        try (right; unfold not in *; intro H';
             subst injections; apply H; reflexivity);
        try (right; unfold not in *; intro H';
             inversion H');
        subst; apply n; reflexivity.
    Qed.

    Lemma eval_bound_inversion:
      forall E s t, 
        eval_bound E s t ->
        (s = t /\ typeis_qcname s) \/
        (s <> t /\
          match t with
            | t_C C => exists X, binds X C E /\ s = t_X X
            | t_CdotC C D => exists X, binds X C E /\ 
                                       s = t_XdotC X D
            | _ => False
          end).
    Proof.
      intros.
      assert (H0 := type_dec s t).
      destruct H0.

      left.
      split.
      assumption.
      subst.
      inversion H; subst.
      assumption.

      right.
      split.
      assumption.
      destruct t.
      inversion H;
        subst.
      exfalso.
      apply H0.
      reflexivity.
      exists X.
      split;
        eauto.
      inversion H;
        subst.
      unfold not in H0.
      apply H0.
      reflexivity.
      inversion H;
        subst.
      exfalso.
      apply H0.
      reflexivity.
      exists X.
      split;
        eauto.
      inversion H;
        subst.
      apply H0.
      reflexivity.
      inversion H;
        subst.
      apply H0.
      reflexivity.
    Qed.

    Lemma sub_eval_at:
      forall E t s T,
        sub E T (t_C s) ->
        eval_at (t, (t_C s)) t ->
        eval_at (t, T) t.
    Proof.
      intros.
      inversion H;
        subst;
        destruct t;
        eauto;
        inversion H0.
    Qed.      

    Lemma sub_eval_at_X:
      forall E t s T,
        sub E T (t_X s) ->
        eval_at (t, (t_X s)) t ->
        eval_at (t, T) t.
    Proof.
      intros.
      inversion H;
        subst;
        destruct t;
        eauto;
        inversion H0.
    Qed.      

    Lemma sub_nested_t:
      forall E T S,
        sub E T S ->
        typeis_nested T ->
        S = T \/ S = (t_C Object).
    Proof.
      intros E T S H.
      induction H;
        intros.
              left. reflexivity.
            inversion H0.
          right. reflexivity.
        destruct (IHsub1 H1).
          subst.
          apply (IHsub2 H1).
        subst.
        apply sub_object_object in H0.
          subst.
          right. reflexivity.
        reflexivity.
      inversion H0.
    Qed.

    Hint Resolve sub_nested_t.

    Lemma sub_t_nested:
      forall E T S,
        sub E T S ->
        typeis_nested S ->
        S = T.
    Proof.
      intros E T S H.
      induction H;
        intros.
              reflexivity.
            inversion H0.
          inversion H.
        assert (H2 := IHsub2 H1).
        subst.
        apply (IHsub1 H1).
      inversion H0.
    Qed.

    Hint Resolve sub_t_nested.

    Lemma sub_tlc_implies_tlc:
      forall E S T s,
        sub E S T ->
        S = t_C s ->
        exists C, T = t_C C.
    Proof.
      intros E S T s H.
      revert s.
      induction H;
        intros.
              exists s.
              assumption.
            discriminate.
          exists Object.
          reflexivity.
        destruct (IHsub1 s).
        assumption.
        apply (IHsub2 x).
        assumption.
      exists D.
      reflexivity.
    Qed.

    Hint Resolve sub_tlc_implies_tlc.

    Lemma sub_var_implies_tlc:
      forall E X T x,
        sub E X T ->
        X = t_X x ->
        X <> T ->
        exists C, T = t_C C.
    Proof.
      intros E X T x H.
      revert x.
      induction H;
        intros.
              exfalso.
              apply H0.
              reflexivity.
            exists C.
            reflexivity.
          exists Object.
          reflexivity.
        destruct (type_dec S T).
          subst T.
          apply (IHsub2 x H1 H2).
        destruct (IHsub1 x).
        assumption.
        assumption.
        apply (sub_tlc_implies_tlc E T U x0 H0 H4).
      inversion H0.
    Qed.

    Hint Resolve sub_var_implies_tlc.

    Lemma sub_var_nested_implies_tlc:
      forall E X T x D,
        sub E X T ->
        X = t_XdotC x D ->
        X <> T ->
        exists C, T = t_C C.
    Proof.
      intros E X T x D H.
      revert x D.
      induction H;
        intros.
              exfalso.
              apply H0.
              reflexivity.
            exists C.
            reflexivity.
          exists Object.
          reflexivity.
        destruct (type_dec S T).
          subst T.
          apply (IHsub2 x D H1 H2).
        destruct (IHsub1 x D).
        assumption.
        assumption.
        apply (sub_tlc_implies_tlc E T U x0 H0 H4).
      inversion H0.
    Qed.

    Hint Resolve sub_var_implies_tlc.

    Lemma ok_type_context:
      forall E C c A1 A2,
        ok_type E C A1 ->
        C = t_C c ->
        ok_type E C A2.
    Proof.
      intros E C c A1 A2 H.
      revert c A2.
      induction H;
        subst injections;
        intros; 
        eauto;
        discriminate.
    Qed.
    
    Lemma sub_implies_ok_type:
      forall E C D c d A1 A2,
        sub E C D ->
        C = (t_C c) ->
        D = (t_C d) ->
        d <> Object ->
        ok_type E D A1 ->
        ok_type E C A2.
    Proof.
      intros E C D c d A1 A2 H.
      revert c d A1 A2.
      induction H;
        intros.
              subst.
              subst injections.
              inversion H2; eauto.
            discriminate.
          subst injections.
          unfold not in H1.
          exfalso. apply H1. reflexivity.
        subst.
        destruct (sub_tlc_implies_tlc E (t_C c) T c H eq_refl).
        subst.
        assert (IH := IHsub2 x d A1 A1 eq_refl eq_refl H3 H4).
        assert (x <> Object). 
          unfold not.
          intro.
          subst.
          assert (Hs := sub_object_object _ _ _ H0 eq_refl).
          subst injections.
          unfold not in H3.
          apply H3. reflexivity.
        apply (IHsub1 c x A1 A2 eq_refl eq_refl H1 IH).
      subst injections.
      eauto.
    Qed.
  
    Lemma sub_var_implies_eval_bound:
      forall E t0 C T S A,
        sub E T S ->
        T = t_X t0 ->
        S = t_C C ->
        C <> Object ->
        ok_type E S A ->
        exists s0, eval_bound E T (t_C s0) /\
                   sub E (t_C s0) S.
    Proof.
      intros E t0 C T S A H.
      revert t0 C A.
      induction H;
        intros;
        subst;
        subst injections.
              inversion H0.
            exists C0.
            split;
              eauto.
          unfold not in H1. exfalso. apply H1. reflexivity.
        destruct (type_dec (t_X t0) T).
          subst.
          apply (IHsub2 t0 C A eq_refl eq_refl).
          assumption.
          assumption.
        assert (t_X t0 <> t_C C).
          unfold not.
          intro.
          inversion H2.
        destruct (sub_var_implies_tlc _ _ _ _ H eq_refl H1).
        subst.
        clear IHsub2.
        assert (x <> Object).
          unfold not. intro. subst.
          assert (Hs := sub_object_object _ _ _ H0 eq_refl).
          subst injections.
          unfold not in H3. apply H3. reflexivity.
        destruct (IHsub1 t0 x A eq_refl eq_refl H5). 
        apply (sub_implies_ok_type _ _ _ _ _ _ _ H0 
                                   eq_refl eq_refl H3 H4).
        exists x0.
        destruct H6.
        split; eauto.
      discriminate.
    Qed.

    Hint Resolve sub_var_implies_eval_bound.

    Lemma field_implies_ok:
      forall C f t A E,
        field (t_C C) f t ->
        typeis_qcname A ->
        ok_type E (t_C C) A.
    Proof.
      intros.
      destruct H.
      revert H1 H0.
      revert A E t f.
      induction H;
        intros;
        eauto.
      inversion H1.
    Qed.

    Hint Resolve field_implies_ok.
      
    (** ** First two generalized typing rules *)
    Lemma gt_field: 
      forall E tE e t T0 A T T' f B,
        ok_type E T0 A ->
        wide_typing E tE e T0 A ->
        typeis_qcname A ->
        field T f T' ->
        eval_bound E B T ->
        eval_at (T', T0) t ->
        eval_at (T0, A) B ->
        typing E tE (e_field e f) t A.
    Proof.
      intros E tE e t T0 A T T' f B Hok H H0 H1 H2 H3 H4.
      inversion H;
        subst.      

      destruct B.
              apply (eval_at_inversion T0 A (t_C s)) in H4; subst.
              inversion H2; subst.
              assert (Heq : t = T').
                inversion H3; eauto.
              subst T'.

              destruct t0.
                      assert (t_C s <> t_C Object).
                        unfold not. intro. subst injections.
                        unfold field in H1.
                        assert (Hf := f_tobject).
                        destruct H1.
                        assert (He := fields_fun _ _ _ H1 Hf).
                        subst.
                        inversion H8.
                      assert (Hs := sub_ok_implies_ok' _ _ _ _ H7 H8 Hok).
                      destruct Hs.
                      assert (Hsf := sub_field E (t_C s0) (t_C s) f t x
                                               (tiq_C s0) H7 H9 H1). 
                      assert (eval_bound E (t_C s0) (t_C s0)).
                        eauto.
                      assert (Hea := sub_eval_at _ _ _ 
                                                   (t_C s0) H7 H3).
                      apply (t_field _ _ _ _ _ _ _ _ _ _
                             H0 Hsf H10 Hea); eauto.
                    assert (s <> Object).
                      unfold not. intro. subst.
                      unfold field in H1.
                      assert (Hf := f_tobject).
                      destruct H1.
                      assert (He := fields_fun _ _ _ H1 Hf).
                      subst.
                      inversion H8.
                    destruct (sub_var_implies_eval_bound 
                                E t0 s _ _ A H7 eq_refl eq_refl) 
                        as [s0 [Heb Hs]]; eauto.
                    assert (t_C s <> t_C Object).
                      unfold not in *. intro. subst injections.
                      apply H8. reflexivity.
                    assert (Ho := sub_ok_implies_ok' _ _ _ _ Hs H9 Hok).
                    destruct Ho.
                    assert (Hsf := sub_field E (t_C s0) (t_C s) f t x
                                     (tiq_C s0) Hs H10 H1). 
                    assert (Hea := sub_eval_at _ _ _ (t_X t0) H7 H3).
                    eapply (t_field _ _ _ _ _ _ _ _ _ _
                           H0 Hsf Heb Hea); eauto.                    
                  apply sub_nested_t in H7. 
                    destruct H7. inversion H7. subst injections.
                    exfalso. eauto. eauto.
                apply sub_nested_t in H7. 
                  destruct H7. inversion H7. subst injections.
                  exfalso. eauto. eauto.
              apply sub_nested_t in H7.
                destruct H7. inversion H7. subst injections.
                exfalso. eauto. eauto.

            inversion H4; subst.
            inversion H2; subst.
              inversion H8.
            assert (T' = t).
              inversion H3;
              subst;
              eauto.
            subst T'.
            destruct t0.
                    assert (Hs : sub E (t_X t1) (t_C C)).
                      inversion H2; subst; eauto.
                    assert (Hs' := s_trans E (t_C s) 
                                           (t_X t1) (t_C C) H7 Hs).
                    assert (t_X t1 <> t_C Object).
                      unfold not. intro. 
                      inversion H8.
                    assert (He := sub_ok_implies_ok' _ _ _ _ H7 H8 Hok).
                    destruct He.
                    assert (Hsf := sub_field E (t_C s) (t_C C) f t x
                                   (tiq_C s) Hs' H9 H1). 
                    assert (eval_bound E (t_C s) (t_C s)). 
                      eauto.
                    assert (Hea := sub_eval_at_X _ _ _ (t_C s) H7 H3).
                    apply (t_field _ _ _ _ _ _ _ _ _ _
                             H0 Hsf H11 Hea); eauto.
                    assert (sub E (t_X t1) (t_C C)).
                      inversion H2; eauto.
                  assert (Hs' := s_trans E (t_X t0) (t_X t1) (t_C C) H7 H8).
                  assert (C <> Object).
                    unfold not. intro. subst.
                    unfold field in H1.
                    assert (Hf := f_tobject).
                    destruct H1.
                    assert (He := fields_fun _ _ _ H1 Hf).
                    subst.
                    inversion H9.
                  destruct (sub_var_implies_eval_bound 
                              E t0 C _ _ A Hs' eq_refl eq_refl) 
                      as [s0 [Heb Hs]]; eauto.
                  assert (t_X t1 <> t_C Object).
                    unfold not. intro. 
                    inversion H11.
                  assert (He := sub_ok_implies_ok _ _ _ _ H8 Hok).
                  destruct He.
                  assert (t_C C <> t_C Object).
                    unfold not in *. intro. subst injections.
                    apply H9. reflexivity.
                  assert (He' := sub_ok_implies_ok' _ _ _ _ Hs H13 H12).
                  destruct He'.
                  assert (Hsf := sub_field E (t_C s0) (t_C C) f t x0
                                           (tiq_C s0) Hs H14 H1). 
                  assert (Hea := sub_eval_at_X _ _ _ (t_X t0) H7 H3).
                  eapply (t_field _ _ _ _ _ _ _ _ _ _
                                  H0 Hsf Heb Hea); eauto.
                apply sub_nested_t in H7.
                  destruct H7. inversion H7. inversion H7. eauto.
              apply sub_nested_t in H7.
                destruct H7. inversion H7. inversion H7. eauto.
            apply sub_nested_t in H7.
              destruct H7. inversion H7. inversion H7. eauto.

          apply (eval_at_inversion T0 A (t_CdotC s s0)) in H4; subst.
          inversion H2; subst.
          destruct H4 as [H4 | [D [H4 H4']]];
            subst;
            subst injections.
            destruct t0.
                    apply sub_t_nested in H7. inversion H7. eauto.
                  apply sub_t_nested in H7. inversion H7. eauto.
                destruct (type_dec (t_CdotC s1 s2) (t_CdotC s s0)).
                  subst injections.
                  assert (t=T' \/ exists D, 
                                    t = t_CdotC s D /\ 
                                    T' = t_dotC D).
                    inversion H3;
                    subst;
                    eauto.
                  destruct H4.
                    subst T'.
                    apply (t_field _ _ _ _ _ _ _ _ _ _
                             H0 H1 H2 H3); eauto.
                  destruct H4 as [D [Ht HT']].
                  subst.
                  apply (t_field _ _ _ _ _ _ _ _ _ _
                               H0 H1 H2 H3); eauto.
                apply sub_t_nested in H7. exfalso. eauto. eauto.
              apply sub_t_nested in H7. inversion H7. eauto.
            apply sub_t_nested in H7. inversion H7. eauto.
          destruct t0.
                  apply sub_t_nested in H7. inversion H7. eauto.
                apply sub_t_nested in H7. inversion H7. eauto.
              apply sub_t_nested in H7. inversion H7. eauto.
            apply sub_t_nested in H7. inversion H7. eauto.
          apply (t_field _ _ _ _ _ _ _ _ _ _
                         H0 H1 H2 H3); eauto.
          destruct (type_dec (t_dotC s1) (t_dotC s0)).
            subst injections.
            eauto.
          apply sub_t_nested in H7. exfalso. eauto. eauto.

        inversion H2; subst.
          inversion H8.
        apply (eval_at_inversion T0 A (t_XdotC t1 s)) in H4; subst.
        inversion H2; subst.
        destruct H4 as [H4 | [D' [H4 H4']]];
          subst;
          subst injections.
          destruct t0.
                  apply sub_t_nested in H7. inversion H7. eauto.
                apply sub_t_nested in H7. inversion H7. eauto.
              apply sub_t_nested in H7. inversion H7. eauto.
            destruct (type_dec (t_XdotC t0 s0) (t_XdotC t1 s)).
              subst injections.
              assert (t=T' \/ exists D, 
                                t = t_XdotC t1 D /\ 
                                T' = t_dotC D).
                inversion H3;
                    subst;
                    eauto.
              destruct H4.
                subst T'.
                apply (t_field _ _ _ _ _ _ _ _ _ _
                               H0 H1 H2 H3); eauto.
              destruct H4 as [D' [Ht HT']].
              subst.
              apply (t_field _ _ _ _ _ _ _ _ _ _
                             H0 H1 H2 H3); eauto.
            apply sub_t_nested in H7. exfalso. eauto. eauto.
          apply sub_t_nested in H7. inversion H7. eauto.
        destruct t0.
                apply sub_t_nested in H7. inversion H7. eauto.
              apply sub_t_nested in H7. inversion H7. eauto.
            apply sub_t_nested in H7. inversion H7. eauto.
          apply sub_t_nested in H7. inversion H7. eauto.
        apply (t_field _ _ _ _ _ _ _ _ _ _
                       H0 H1 H2 H3); eauto.
        destruct (type_dec (t_dotC s0) (t_dotC s)).
          inversion H0.
        apply sub_t_nested in H7. exfalso. eauto. eauto.
        
      inversion H4; subst.
      inversion H0.
    Qed.                  
    
    Hint Resolve gt_field.
    
    Lemma gt_sub : 
      forall E tE e t t' A,
        wide_typing E tE e t A ->
        sub E t t' ->
        wide_typing E tE e t' A.
    Proof.
      destruct 1; eauto.
    Qed.
    
    (* To avoid needless search, only hint gt_sub when the sub relation is already in context; similar in spirit to "Hint Immediate gt_sub." but a little more powerful *)
    Hint Extern 1 (wide_typing ?E ?e ?t) =>
    match goal with
      | H: sub ?t0 t |- _ => refine (gt_sub E e t0 t _ H)
    end.

    Definition ok_ct_class C D fs k ms ns := 
      ok_ctable_class _ C D fs k ms ns ok_ct.

    Definition ok_ct_nclass C D fs ms k ns F fs' k' ms' := 
      ok_ctable_nclass _ C D fs ms k ns F fs' k' ms' ok_ct.

    Definition ok_ct_meth C D fs k ms ns m t tE E e H :=
        ok_class_meth C D fs ms m t E tE e k ns 
                      (ok_ct_class _ _ _ _ _ _ H).

    Definition ok_ct_nmeth C D fs k ms ns m t tE E e F fs' k' ms' H H2 :=
        ok_nclass_meth C D fs ms m t E tE e k ns F fs' k' ms'
                      (ok_ct_class _ _ _ _ _ _ H)
                      (ok_ct_nclass _ _ _ _ _ _ _ _ _ _ H H2).

    Hint Resolve ok_ct_class ok_ct_nclass ok_ct_meth ok_ct_nmeth.

    Lemma extends_fun:
      forall C D D',
        extends C D ->
        extends C D' ->
        D = D'.
    Proof.
      intros.
      unfold extends in *.
      destruct H as [fs [c [ms [ns H]]]].
      destruct H0 as [fs' [c' [ms' [ns' H0]]]].
      apply binds_fun with (a:=(D,fs,c,ms,ns)) in H0.
      subst injections.
      reflexivity.
      assumption.
    Qed.

    Lemma ok_type_weaker:
      forall E C A,
        ok E ->
        ok_type nil C A ->
        ok_type E C A.
    Proof.
      intros E C A H.
      revert C A.
      induction H;
        intros.
      assumption.
      assert (H2 := IHok C A H1).
      apply ok_cons with (v:=v) in H0.
      apply (ok_type_weak E ((x,v) :: E) C A x v eq_refl H0 H2).
      assumption.
    Qed.

    Lemma ok_no_env:
      forall E T A,
        ok_type nil T A ->
        ok_type E T A.
    Proof.
      intros.
      induction H; eauto.
      inversion H.
      inversion H0.
    Qed.

    Lemma sub_extends_eq:
      forall E C D T t,
        sub E T t ->
        T = t_C C ->
        extends C D ->
        T = t \/ sub E (t_C D) t.
    Proof.
      intros E C D T t H.
      revert C D.
      induction H;
        intros;
        subst.
      left; reflexivity.
      inversion H0.
      right.
      apply s_object.
      destruct (type_dec (t_C C) U).
        subst.
        left; reflexivity.
      destruct (IHsub1 C D eq_refl H2).
      subst.
      right.
      destruct (IHsub2 C D eq_refl H2).
      subst.
      exfalso. 
      apply H1.
      reflexivity.
      assumption.
      right.
      eauto.
      subst injections.
      right.
      assert (extends C0 D).
        unfold extends.
        eauto.
      apply (extends_fun C0 D D0) in H1.
        subst.
        eauto.
      assumption.
    Qed.

    (** ** Method body conforms to method type *)
    Fact method_implies_typing: 
      forall m t E t0 tE e,
        method m t E t0 tE e ->
        typeis_top t ->
        exists t' A, 
          sub E t t' /\
          wide_typing E ((this,t')::tE) e t0 A.
    Proof.
      intros.
      remember t0 as t0'.
      induction H;
        subst.
              eauto via (ok_meth env t0 m tenv e (t_C C)).
              exists x, (t_C C).
              inversion H4; subst.
              split;
                eauto.
            destruct (IHmethod eq_refl (tit1 D)) as [t [A [H3 H4]]].
            exists t, A.
            apply s_class with (env:=env)in H.
            split; 
              eauto.
          inversion H0.
        inversion H0.
      inversion H0.
    Qed.

    Hint Resolve method_implies_typing.
 
    (** ** Subtyping preserves method types *)
    Fact sub_mtype: 
      forall u u' t m env t0 tenv te E,
        sub E u t ->
        method m t env t0 tenv te ->
        eval_bound E u u' ->
        exists ue, method m u' env t0 tenv ue.
    Proof.
      intros u u' t m env t0 tenv te E H.
      revert u' m env t0 tenv te.
      induction H; intros.
              assert (T = u').
                assert (typeis_qcname T).
                  inversion H; subst; eauto.
                inversion H0; subst; eauto.
                  inversion H1.
                inversion H1.
              subst.
              eauto.
            assert (u' = t_C C).
              inversion H1; subst. 
                inversion H2.
              apply (binds_fun H4) in H.
              subst.
              reflexivity.
            subst.
            eauto.
          assert (H3 := obj_nomeths m env tenv t0 te).
          exfalso.
          apply H3.
          assumption.
        destruct (type_dec S T); subst.
          apply IHsub2 with (te:=te); eauto.
        destruct S.
                assert (u' = t_C s).
                  inversion H2; subst.
                  reflexivity.
                subst.
                destruct (IHsub2 T m env t0 tenv te); eauto.
              assert (typeis_qcname T).
                apply sub_var_implies_tlc with (x:=t) in H; eauto.
                destruct H as [C HC].
                subst.
                eauto.
              destruct (IHsub2 T m env t0 tenv te); eauto.
            assert (typeis_qcname T).
              apply sub_nested_t in H; eauto.
              destruct H as [HC | HT].
                subst.
                eauto.
              subst.
              eauto.
            destruct (IHsub2 T m env t0 tenv te); eauto.            
          assert (typeis_qcname T).
            apply sub_nested_t in H; eauto.
            destruct H as [HC | HT].
              subst.
              exfalso. apply H3. reflexivity.
            subst.
            eauto.
          destruct (IHsub2 T m env t0 tenv te); eauto.
        apply sub_nested_t in H; eauto.
        destruct H as [HC | HT].
          subst.
          exfalso. apply H3. reflexivity.
        subst.
        apply sub_object_object in H0; eauto.
        subst.
        assert (Ho := obj_nomeths m env tenv t0 te).
        contradiction (Ho H1).
      assert (t_C C = u').
        inversion H1; subst; eauto.
      subst.
      assert (extends C D).
        unfold extends.
        eauto.
      remember (get m ms) as P.
      destruct P.
        destruct p as [[[pE pT] ptE] pe].
        assert (binds m (pE,pT,ptE,pe) ms).
          unfold binds.
          symmetry.
          assumption.
        assert (ok_tclass C D fs c ms ns).
          eauto.
        unfold ok_tclass in H4.
        destruct H4 as [A' [gs [_ [_ [H5 _]]]]].
        assert (ok_meth' (t_C C) m (pE,pT,ptE,pe)).
          apply binds_forall_method with (ms:=ms).
            assumption.
          assumption.
        unfold ok_meth' in H4.
        unfold ok_meth in H4.
        destruct H4 as [B [_ [_ [_ [_ [_ [_ H7]]]]]]].
        destruct (H7 (t_C D) env t0 tenv te)
          as [H8 [H9 H10]]; eauto.
        subst.
        exists pe.
        eauto.
      assert (no_binds m ms).
        unfold no_binds.
        symmetry.
        assumption.
      apply (mt_tsuper C D fs c m ms ns env tenv t0 te) in H0.
          exists te.
          assumption.
        assumption.
      assumption.
      Grab Existential Variables.
      exact env.
    Qed.

    Hint Resolve sub_mtype.      

    Lemma sub_var_implies_bound:
      forall E x X T,
        sub E X T ->
        T <> t_C Object ->
        X = t_X x ->
        typeis_qcname T ->
        exists t, eval_bound E X t.
    Proof.
      intros E x X T H.
      revert x.
      induction H; intros; subst; eauto.
      unfold not in H. exfalso. apply H. reflexivity.
      destruct (type_dec (t_X x) T).
      subst.
      apply (IHsub2 x H1 eq_refl H3).
      apply sub_var_implies_tlc with (x:=x)in H; eauto.
      destruct H; subst.
      assert (t_C x0 <> t_C Object).
        unfold not. intro. subst injections.
        assert (Hs := sub_object_object _ _ _ H0 eq_refl).
        subst.
        unfold not in H1.
        apply H1. reflexivity.
      apply (IHsub1 x H eq_refl); eauto.
    Qed.
      
    Lemma eval_at_subst_sub:
      forall XPs U U' t0 T0 t E,
        eval_at (U', T0) t ->
        U' = subst_type XPs U ->
        sub E t0 T0 ->
        eval_at (subst_type XPs U, t0) t.
    Proof.
      intros XPs U U' t0 T0 t E H0 H.
      revert H0. 
      revert t0 T0 t E.
      induction H; 
        intros; 
        eauto.
      inversion H0; subst; eauto.
      assert (Hs := sub_t_nested _ _ _ H (tin1 C B)).
      subst. eauto.
      assert (Hs := sub_t_nested _ _ _ H (tin2 X B)).
      subst. eauto.
      assert (Hs := sub_t_nested _ _ _ H (tin3 C)).
      subst. eauto.
    Qed.      

    Lemma eval_ats_subst_sub:
      forall XPs xTs T0 ts E t0,
        eval_ats (subst_types XPs (imgs xTs))  T0 ts ->
        sub E t0 T0 ->
        eval_ats (subst_types XPs (imgs xTs)) t0 ts.
    Proof.
      intros XPs xTs T0 ts E t0 H.
      induction H; intros; subst.
      eauto.
      apply ca_cons.
      assert (H2 := eval_at_subst_sub nil u (subst_type nil u) t0 t1 t E).
      unfold subst_type in H2.
      apply H2.
      assumption.
      reflexivity.
      assumption.
      apply IHeval_ats.
      assumption.
    Qed.
          
    Lemma sub_t_not_Object:
      forall E S T,
        sub E S T ->
        T <> t_C Object ->
        S <> t_C Object.
    Proof.
      intros E S T H.
      induction H; 
        intros;
        subst;
        eauto.
      unfold not.
      intro.
      discriminate.
      unfold not.
      intro.
      subst injections.
      apply (binds_object (D,fs,c,ms,ns) H).
    Qed.

    Lemma sub_t_top_implies_top:
      forall E S T,
        sub E T S ->
        typeis_top S ->
        S <> t_C Object ->
        typeis_top T.
    Proof.
      intros.
      induction H; subst; eauto.
        unfold not in H1.
        exfalso. apply H1. reflexivity.
      apply IHsub1.
      apply IHsub2.
      assumption.
      assumption.
      assert (Hs := sub_t_not_Object _ _ _ H2 H1).
      assumption.
    Qed.

    Lemma eval_at_sub':
      forall E t0 T0 A B,
        sub E t0 T0 ->
        T0 <> t_C Object ->
        eval_at (T0, A) B ->
        typeis_qcname A ->
        exists B', sub E B' B /\ eval_at (t0, A) B'.
    Proof.
      intros.
      inversion H1; subst.
                  assert (HsT := sub_t_nested _ _ _ H (tin3 D)).
                  subst; eauto.
                assert (Hs := sub_t_nested _ _ _ H (tin3 D)). 
                subst. eauto.
              assert (Hs := sub_t_nested _ _ _ H (tin3 D)).
              subst; eauto.
            assert (Hs := sub_t_top_implies_top _ _ _ H (tit1 C) H0).
            inversion Hs; subst; eauto.
          assert (Hs := sub_t_top_implies_top _ _ _ H (tit2 X) H0).
          inversion Hs; subst; eauto.
        assert (Hs := sub_t_nested _ _ _ H (tin1 D C)).
        subst; eauto.
      assert (Hs := sub_t_nested _ _ _ H (tin2 X C)).
      subst; eauto.      
    Qed.      

    (** ** One more generalized typing rule *)
    Lemma gt_meth : 
      forall A Ps XPs U T0 t Us ts XCs Cs xTs m C b B E tE e0 es,
        typeis_qcname A ->
        typesare_famname Ps ->
        eval_at (subst_type XPs U, T0) t ->
        eval_ats (subst_types XPs Us) T0 ts ->
        keys XPs = keys XCs ->
        imgs XPs = Ps ->
        imgs XCs = Cs ->
        imgs xTs = Us ->
        method m C XCs U xTs b ->
        eval_bound E B C ->
        eval_at (T0, A) B ->
        wide_typing E tE e0 T0 A ->
        wide_typings E tE es ts A ->
        subs E Ps Cs -> 
        wide_typing E tE (e_meth e0 m Ps es) t A.
    Proof.
      intros.
      inversion H10; subst.
      apply (wt_sub E tE _ t t A).
          assumption.
        Focus 2. apply s_refl.
      destruct (type_dec T0 (t_C Object)) as [Heq | Hneq].
        subst.
        inversion H9; subst.
        inversion H8; subst.
        assert (Hobj := obj_nomeths m XCs xTs U b).
        unfold not in Hobj. exfalso. apply Hobj. assumption.
      assert (HB' := eval_at_sub' _ _ _ _ _ H15 Hneq H9 H).
      destruct HB' as [B' [HBs HBe]].
      destruct B'.
              inversion HBe; subst.
              assert (Hsub := sub_tlc_implies_tlc _ _ _ _ HBs eq_refl).
              destruct Hsub as [b' Hb]; subst.
              inversion H9; subst.
              inversion H8; subst.
              assert (Hb : eval_bound E (t_C s) (t_C s)).
               apply be1. eauto.
              assert (Hsm := sub_mtype _ _ _ _ _ _ _ _ _ 
                                       H15 H7 Hb).
              destruct Hsm as [ue Hm].
              eapply t_invk with (T0:=t_C s); eauto.
                apply (eval_at_subst_sub _ _ _ _ _ _ _ H1 eq_refl H15).
              apply (eval_ats_subst_sub _ _ _ _ _ _ H2 H15).
            inversion HBe; subst.
            destruct B.
              assert (t_C s = C).
                inversion H8; subst.
                reflexivity.
              subst.
              assert (ok_type E (t_C s) A).
                inversion H7; subst; eauto.
              assert (s <> Object).
                unfold not. intro. subst.
                assert (Ho := obj_nomeths m XCs xTs U b).
                unfold not in Ho.
                apply Ho. assumption.
              assert (Hsv := sub_var_implies_eval_bound _ _ _ _ _ _ 
                               HBs eq_refl eq_refl H5 H4).
              destruct Hsv as [s0 [Heb Hs]].
              inversion H9; subst.
              assert (Hsm := sub_mtype _ _ _ _ _ _ _ _ _ 
                                     H15 H7 Heb).
              destruct Hsm as [ue Hm].
              eapply t_invk with (T0:=t_X t1); eauto.
                apply (eval_at_subst_sub _ _ _ _ _ _ _ H1 eq_refl H15).
              apply (eval_ats_subst_sub _ _ _ _ _ _ H2 H15).
            inversion H9; subst.
            destruct (type_dec (t_X t1) (t_X t0)).
              subst injections.
              eapply t_invk with (T0:=t_X t0); eauto.
            destruct (sub_var_implies_tlc _ _ _ t1 H15 eq_refl H4)
                as [C' HC].
            inversion HC.

          apply sub_var_implies_tlc with (x:=t1) in HBs.          
              inversion HBs.
              discriminate.
            reflexivity.
          unfold not.
          intro.
          discriminate.
        apply sub_var_implies_tlc with (x:=t1) in HBs.          
            inversion HBs.
            discriminate.
          reflexivity.
        unfold not.
        intro.
        discriminate.
      apply sub_var_implies_tlc with (x:=t1) in HBs.          
          inversion HBs.
          discriminate.
        reflexivity.
      unfold not.
      intro.
      discriminate.

          assert (Hsub := sub_nested_t _ _ _ HBs (tin1 s s0)).
          destruct Hsub as [Hsub1 | Hsub2].
            subst.
            inversion H8; subst.
            inversion HBe; subst.
              assert (Hsub := sub_nested_t _ _ _ H15 (tin3 s0)).
              destruct Hsub as [Hsub1 | Hsub2].
                subst.
                eapply t_invk with (T0:=t_dotC s0); eauto.                
              subst.
              inversion H9.
            eapply t_invk with (T0:=t_CdotC s s0); eauto.
            assert (Hsub := sub_nested_t _ _ _ H15 (tin1 s s0)).
              destruct Hsub as [Hsub1 | Hsub2].
                subst.
                assumption.
              subst.
            inversion H9; subst.
          apply (eval_ats_subst_sub _ _ _ _ _ _ H2 H15).
        subst.
        inversion H8; subst.
        assert (Hobj := obj_nomeths m XCs xTs U b).
        unfold not in Hobj.
        exfalso. apply Hobj. assumption.
      
        assert (Hsub := sub_nested_t _ _ _ HBs (tin2 t1 s)).
          destruct Hsub as [Hsub1 | Hsub2].
            subst.
            inversion H8; subst.
              inversion H7.
            inversion HBe; subst.
              assert (Hsub := sub_nested_t _ _ _ H15 (tin3 s)).
              destruct Hsub as [Hsub1 | Hsub2].
                subst.
                eapply t_invk with (T0:=t_dotC s); eauto.
              subst.
              inversion H9.
            eapply t_invk with (T0:=t_XdotC t1 s); eauto.
              apply (eval_at_subst_sub _ _ _ _ _ _ _ H1 eq_refl H15).
            assert (Hsub := sub_nested_t _ _ _ H15 (tin2 t1 s)).
              destruct Hsub as [Hsub1 | Hsub2].
                subst.
                assumption.
              subst.
            inversion H9; subst.
          subst.
          inversion H8; subst.
          assert (Hobj := obj_nomeths m XCs xTs U b).
          unfold not in Hobj.
          exfalso. apply Hobj. assumption.
      
        assert (Hsub := sub_nested_t _ _ _ HBs (tin3 s)).
          destruct Hsub as [Hsub1 | Hsub2].
            subst.
            inversion H8; subst.
              inversion H7.
            subst.
          inversion H8; subst.
          assert (Hobj := obj_nomeths m XCs xTs U b).
          unfold not in Hobj.
          exfalso. apply Hobj. assumption.
    Qed.

    Hint Resolve gt_meth.

End OkTableAndNoObjFacts.
